x:Id, t:Type, v:t. x : t initially x = v  MsgA 

latex

Definitions	Void, Knd, x.A(x), x:A. B(x), x. t(x), 2of(t), IdDeq, f(x)?z, type List, , IdLnk, x:AB(x), Top, x:AB(x), State(ds), Prop, x:A. B(x), mk-ma, x : t initially x = v, MsgA, x : v, Type, Id, a:A fp B(a), t  T
Lemmas	mk-ma wf, fpf-cap-single1, ma-state wf, top wf, IdLnk wf, fpf-empty wf, fpf-single wf, fpf-cap wf, id-deq wf, pi2 wf, Id wf, Knd wf